In recent years, a design of a document such as a Web page available on the Internet becomes various. Although a well-designed Web page looks good, a particular user such as a visually handicapped person may not understand the Web page very well. Moreover, when a structure of a page violates a syntax rule, some kinds of Web browsers may not display the page correctly. Therefore, there have been conventionally proposed some systems that determine whether a document such as a Web page satisfies a prepared specification to evaluate the easiness of understanding or designate a point to be corrected in the page. See, for example, Non-Patent Documents (8) and (9). Moreover, researches for prescribing a specification of a structured document such as HTML or XML and researches for a schema or the like for prescribing a specification have been advanced. See, for example, Non-Patent Documents (2), (4), and (5).
Non-Patent Documents
(1) Yasuhiko Minamide, “Static approximation of dynamically generated Web pages”, World Wide Web (WWW), 2005
(2) FDR2 (Formal Systems)
(3) Cristiano Calcagno, Philippa Gardner, Uri Zarfaty, “Context Logic and Tree Update”, Principles of Programming Languages (POPL), 2005
(4) Eugenio Di Sciascio, Francesco M. Donini, Marina Mongiello, Giacomo Piscitelli, “Web applications design and maintenance using Symbolic Model Checking”, European Conference On Software Maintenance And Reengineering (CSMR), 2003
(5) Eun-Hye CHOI, Hiroshi Watanabe, “Modeling and Verification of Class Specification for Web Applications”, Japan Symposium on Software Testing
(6) H. Comon, et al., “Tree Automata Techniques and Applications”, http://www.grappa.univ-lille3.fr/tata/, 1997
(7) Haruo Hosoya and Benjamin Pierce, “Regular expression pattern matching for XML”, Principles of programming languages (POPL), 2001
(8) aDesigner (IBM)
(9) Dreamweaver 8 (Macromedia)
(10) KazunoriWashioetal., “Syntax Verification Technique Using Data Flow Analysis for Java Script Embedded HTML Documents”, Technical Report of IEICE, SS2002-22, Vol. 102, No. 370, pp. 13-18,
(11) Takaaki Tateishi, et al., “Accessibility Checking Tool for DHTML”, http://spa.jssst.or.jp/2006/, SPA2006
Some Web pages may include not only static images but also moving images. For example, Flash of Macromedia company or Dynamic HTML are used as a standard to generate moving images. The moving images are realized by sequentially switching the display of static images by means of a program supplied with a Web page. If we try to apply the technologies concerning static images to moving images, it is necessary to actually execute the program and determine whether the specification is satisfied by each static image generated as a result of the execution. However, in case that it is determined whether all static images to be displayed satisfy the specification, the execution states of the program explosively increase. Therefore, the determination may not be completed in realistic time.
In addition, there has been proposed a technique for analyzing a status after executing a program without executing the program. See, for example, Non-Patent Documents (1), (3), (10), and (11). According to techniques of Non-Patent Documents (1) and (10), a character string to be generated by executing a program can be analyzed without really executing the program. However, according to these techniques, it is not possible to analyze how to change data with a tree structure described in HTML, XML or the like as a result of executing a program. Moreover, Non-Patent Document (3) discloses logic for determining whether data with a tree structure obtained by executing a program satisfy a specification. However, this document does not disclose how an information-processing apparatus determines satisfaction of specifications on the basis of this logic automatically. Moreover, Non-Patent Document (11) discloses that a technique for analyzing a character string generated as a result of executing a program should be applied to DOM (document object model) with a tree structure. However, Non-Patent Document (11) does not disclose a concrete method for applying the technique.